Nuprl Lemma : fpf-accum_wf
11,40
postcript
pdf
A
,
C
:Type,
B
:(
A
Type),
x
:
a
:
A
fp
B
(
a
),
y
:
C
,
f
:(
C
(
a
:
A
B
(
a
)
C
)).
fpf-accum(
z
,
a
,
v
.
f
(
z
,
a
,
v
);
y
;
x
)
C
latex
Definitions
fpf-accum(
z
,
a
,
v
.
f
(
z
;
a
;
v
);
y
;
x
)
,
t
T
,
a
:
A
fp
B
(
a
)
,
x
(
s
)
,
x
.
t
(
x
)
,
x
:
A
.
B
(
x
)
,
x
(
s1
,
s2
,
s3
)
,
x
,
y
.
t
(
x
;
y
)
,
list_accum(
x
,
a
.
f
(
x
;
a
);
y
;
l
)
,
(
x
l
)
Lemmas
list-subtype
,
list
accum
wf
,
l
member
wf
,
fpf
wf
origin
A, C:Type, B:(A
Type), x:a:A fp B(a), y:C, f:(C(a:AB(a)C)).
C A, C:Type, B:(AType), x:a:A fp B(a), y:C, f:(C(a:AB(a)C)).
C T B(a)
x. t(x)x:A. B(x)x,y. t(x;y) l)